This is neat! I like how short and simple everything is.

I do need to think a bit more about what to do with the Context. I might want to just make it a global shared variable for the purpose of the python bindings, similar to what Z3 does.

Should be a fairly small/easy fix if we decide to refactor to a global Context, i.g.? Is multi-threading a concern?

Should be a fairly small/easy fix if we decide to refactor to a global Context, i.g.? Is multi-threading a concern?

Currently your binding has a combination of a context and a TransitionSystem, but I am not sure how far you can get with that. The alternative would be to allow users to specify a Context for every function call that needs one, but provide a default global Context that everything can use. That is how I imagine the z3 Python bindings work.

In terms of API, 90% of functionality is probably going to be similar to z3 and pySMT, so borrowing the API of one or the other might make sense instead of coming up with our own custom representation.

Here are some use cases I would like to see to make sure the Python API works in these situations before merging it:

1. construct a bit vector formula
2. construct a simple transition system
3. load a transition system from btor
4. analyze a transition system, e.g., extract all array stores and display the expression for the index
5. create an instance of a transition system simulater (the interpreter) and simulate a couple of steps
6. run BMC on a transition system and print out the witness

That might be a bit too ambitious though. Do you know which use case would be the most relevant for you at this moment?